%==================================================================================================
% LUKE PHD THESIS BIBTEX FILE
% ---------------------------
% Sorted chronologically
%==================================================================================================

@article{Hoare78,
   author      = {C. A. R. Hoare},
   title       = {Communicating sequential processes},
   journal     = {Communications of the ACM},
   volume      = {26},
   number      = {1},
   year        = {1983},
   issn        = {0001-0782},
   pages       = {100--106},
   doi         = {10.1145/357980.358021},
   publisher   = {ACM},
   address     = {New York, NY, USA},
   abstract    = {This paper suggests that input and output are basic primitives of programming 
and that parallel composition of communicating sequential processes is a fundamental program 
structuring method. When combined with a development of Dijkstra's guarded command, these concepts 
are surprisingly versatile. Their use is illustrated by sample solutions of a variety of familiar 
programming exercises.}
}


%SORTED AND FORMATTED TO HERE



@incollection {EC80,
   author          = {Emerson, E. and Clarke, Edmund},
   affiliation     = {Harvard University Aiken Computation Laboratory 02138 Cambridge Mass. USA 
02138 
   Cambridge Mass. USA},
   title           = {Characterizing correctness properties of parallel programs using fixpoints},
   booktitle       = {Automata, Languages and Programming},
   series          = {Lecture Notes in Computer Science},
   editor          = {de Bakker, Jaco and van Leeuwen, Jan},
   publisher       = {Springer Berlin / Heidelberg},
   isbn            = {},
   pages           = {169-181},
   volume          = {85},
   doi             = {10.1007/3-540-10003-2_69},
   year            = {1980},
   abstract        = {We have shown that correctness properties of parallel programs can be 
described using 
   computation trees and that from these descriptions fixpoint characterizations can be generated. 
We have 
   also given conditions on the form of computation tree descriptions to ensure that a correctness 
property 
   can be characterized using continuous fixpoints. A consequence is that a correctness property 
such as 
   inevitability under fair scheduling can be characterized as the least fixpoint of a monotonic, 
   noncontinuous transformer, but cannot be characterized using fixpoints of continuous 
transformers (nor as 
   the greatest fixpoint of a monotonic transformer of any degree of complexity lower than fair 
inevitability 
   itself). Hence, currently known proof rules are not applicable (see however [FS80]). We are now 
   investigating whether useful proof rules can exist for correctness properties having only a 
monotonic, 
   noncontinuous least fixpoint characterization. In addition, we are examining alternate notions 
of fairness 
   which do have continuous fixpoint characterizations.}
}

@incollection{QS82,
   author          = {Queille, J. and Sifakis, J.},
   affiliation     = {Laboratoire IMAG BP 53X 38041 Grenoble Cedex France BP 53X 38041 Grenoble 
Cedex France},
   title           = {Specification and verification of concurrent systems in CESAR},
   booktitle       = {International Symposium on Programming},
   series          = {Lecture Notes in Computer Science},
   editor          = {Dezani-Ciancaglini, Mariangiola and Montanari, Ugo},
   publisher       = {Springer Berlin / Heidelberg},
   isbn            = {},
   pages           = {337-351},
   volume          = {137},
   doi             = {10.1007/3-540-11494-7_22},
   year            = {1982},
   abstract        = {The aim of this paper is to illustrate by an example, the alternating bit 
protocol, the 
   use of CESAR, an interactive system for aiding the design of distributed applications. CESAR 
allows the 
   progressive validation of the algorithmic description of a system of communicating sequential 
processes 
   with respect to a given set of specifications. The algorithmic description is done in a high 
level language 
   inspired from CSP and specifications are a set of formulas of a branching time logic, the 
temporal 
   operators of which can be computed iteratively as fixed points of monotonic predicate 
transformers. The 
   verification of a system consists in obtaining by automatic translation of its description 
program an 
   Interpreted Petri Net representing it and evaluating each formula of the specifications.}
}

@article{CES86,
   author          = {Clarke, E. M. and Emerson, E. A. and Sistla, A. P.},
   title           = {Automatic verification of finite-state concurrent systems using temporal 
logic 
   specifications},
   journal         = {ACM Trans. Program. Lang. Syst.},
   volume          = {8},
   number          = {2},
   year            = {1986},
   issn            = {0164-0925},
   pages           = {244--263},
   doi             = {10.1145/5397.5399},
   publisher       = {ACM},
   address         = {New York, NY, USA},
   abstract        = {We give an efficient procedure for verifying that a finite-state concurrent 
system meets 
   a specification expressed in a (propositional, branching-time) temporal logic. Our algorithm 
has complexity 
   linear in both the size of the specification and the size of the global state graph for the 
concurrent 
   system. We also show how this approach can be adapted to handle fairness. We argue that our 
technique can 
   provide a practical alternative to manual proof construction or use of a mechanical theorem 
prover for 
   verifying many finite-state concurrent systems. Experimental results show that state machines 
with several 
   hundred states can be checked in a matter of seconds.}
}



@article{CK01,
   author          = {Janet Carmenates and Matthew R. Keith},
   title           = {Impact of automation on pharmacist interventions and medication errors in a correctional 
health care system},
   journal         = {American Journal of Health-System Pharmacy},
   volume          = {59},
   number				= {9},
   month				= {May},
   year            = {2001},
   pages           = {779--783},
   issn            = {1079-2082},
   publisher       = {American Society of Health-System Pharmacists},
   address         = {Bethesda, MD USA},
   abstract        = {The implementation and impact of an automated check-and-sortation system in a 
correctional health care system are described. In February 1998 the Managed Health Care Division of the 
University of Houston College of Pharmacy submitted a proposal to the Texas State Board of Pharmacy for 
installing an automated check-and-sortation device in its distributive system serving Texas Department of 
Criminal Justice offenders. The new system would eliminate final visual verification of medication orders 
by pharmacists and thereby give them more time for in-depth reviews of patient profiles and for 
recommending clinical interventions. A vendor interested in developing a prototypic automated system was 
identified, and a disease management training course was developed to enable staff pharmacists to provide 
evidence-based pharmacotherapy recommendations. Twelve months of data before automation (February 1997 to 
January 1998) were compared with 16 months of postautomation data (June 1998 to September 1999). The number 
of clinical interventions increased from 396 per 100,000 medication orders filled before automation to 1075 
per 100,000 orders after automation. Dispensing errors decreased from 6.3 to 4.1 per 100,000 medication 
orders filled. Identified filling errors increased from 224 to 256 per 100,000 orders. The reliability of 
the automated system was evidenced by a dispensing error rate of 0.6 per 100,000 orders. Implementation of 
an automated check-and-sortation device in a correctional health care system appeared to reduce dispensing 
errors and give pharmacists more time to review patient profiles and recommend clinical interventions.}
}

@article{BRF01,
   author          = {C. A. Bond and C. L. Raehl and T. Franke},
   title           = {Medication Errors in United States Hospitals},
   journal         = {The Journal of Human Pharmacology and Drug Therapy},
   volume          = {21},
   number				= {9},
   month				= {September},
   year            = {2001},
   doi					= {10.1592/phco.21.13.1023.34617},
   pages           = {1023--1036},
   issn            = {0277-0008},
   publisher       = {IOS Press},
   address         = {Amsterdam, Netherlands},
   abstract        = {This study evaluated hospital demographics, staffing, pharmacy variables, health care 
outcomes measures (severity of illness-adjusted mortality rates, drug costs, total cost of care, and length 
of stay) and medication errors. A database was constructed from the 1992 American Hospital Association's 
Abridged Guide to the Health Care Field, the 1992 National Clinical Pharmacy Services database, and 1992 
mortality data from the Health Care Financing Administration. Simple statistical tests and a severity of 
illness-adjusted multiple regression analysis were employed. The study population consisted of 1116 
hospitals that reported information on medication errors and 913 hospitals that reported information on 
medication errors that adversely affected patient care outcomes. We evaluated factors associated with the 
430,586 medication errors and 17,338 medication errors that adversely affected patient care outcomes. 
Medication errors occurred in 5.07% of the patients admitted each year to these hospitals. Each hospital 
%experienced a medication error every 22.7 hours (every 19.73 admissions). Medication errors that adversely 
%affected patient care outcomes occurred in 0.25% of all patients admitted to these hospitals/year. Each 
%hospital experienced a medication error that adversely affected patient care outcomes every 19.23 days (or 
%every 401 admissions). The following factors were associated with increased medication errors/occupied 
%bed/year: lack of pharmacy teaching affiliation (slope = 0.8875, p=0.0416), centralized pharmacists (slope 
%= 1.0942, p=0.0001), number of registered nurses/occupied bed (slope = 1.624, p=0.032), number of 
%registered pharmacists/occupied bed (slope = 25.0573, p=0.0001), hospital mortality rate (slope = 2.8017, 
%p=0.0192), and total cost of care/occupied bed/year (slope = 0.01432, p=0.0091). Factors associated with 
%decreased medication errors were location in the Mid-Atlantic census region (slope = -1.5182, p=0.03), 
%affiliation with a pharmacy teaching program (slope = -1.0252, p=0.0349), decentralized pharmacists (slope 
%= -0.9843, p=0.0037), and number of medical residents/occupied bed (slope = -1.478, p=0.0014). There was a 
%45% decrease in medication errors (1.81-fold decrease) in hospitals that had decentralized pharmacists, 
%compared with hospitals that had centralized pharmacists. In addition, there was a 94% decrease in 
%medication errors that adversely affected patient care outcomes (16.88-fold decrease) in hospitals that had 
%decentralized pharmacists compared with hospitals that had only centralized pharmacists. Based on previous 
%field studies and our findings in 1116 hospitals, it appears that one of the most effective ways to prevent 
%or reduce medication errors is to decentralize pharmacists to patient care areas. The results of this study 
%should help hospitals reduce the number of medication errors that occur each year.}
}

@article{HCG04,
   author          = {P. Y. Han and I. D. Coombes and B. Green},
   title           = {Factors predictive of intravenous fluid administration errors in Australian surgical 
care wards},
   journal         = {Quality and safety in health care},
   volume          = {14},
   year            = {2004},
   doi					= {10.1136/qshc.2004.010728},
   pages           = {179--184},
   issn            = {1475-3898},
   publisher       = {BMJ Pub. Group},
   address         = {London, England},
   abstract        = {Background: Intravenous (IV) fluid administration is an integral component of clinical 
care. Errors in administration can cause detrimental patient outcomes and increase healthcare costs, 
although little is known about medication administration errors associated with continuous IV infusions. 
Objectives: (1) To ascertain the prevalence of medication administration errors for continuous IV infusions 
and identify the variables that caused them. (2) To quantify the probability of errors by fitting a 
logistic regression model to the data. Methods: A prospective study was conducted on three surgical wards 
at a teaching hospital in Australia. All study participants received continuous infusions of IV fluids. 
Parenteral nutrition and non-electrolyte containing intermittent drug infusions (such as antibiotics) were 
excluded. Medication administration errors and contributing variables were documented using a direct 
observational approach. Results: Six hundred and eighty seven observations were made, with 124 (18.0%) 
%having at least one medication administration error. The most common error observed was wrong 
%administration rate. The median deviation from the prescribed rate was −47 ml/h (interquartile range −75 to 
%+33.8 ml/h). Errors were more likely to occur if an IV infusion control device was not used and as the 
%duration of the infusion increased. Conclusions: Administration errors involving continuous IV infusions 
%occur frequently. They could be reduced by more common use of IV infusion control devices and regular 
%checking of administration rates.}
}

@inproceedings{PP06, 
   author 			= {J. Puustjärvi and L. Puustjärvi}, 
   booktitle 		= {2006 8th International Conference on e-Health Networking, Applications and 
   Services (Healthcom 2006)}, 
   title 				= {Automating the coordination of electronic prescription processes}, 
   year 				= {2006}, 
   month 				= {August}, 
   volume				= {}, 
   number				= {}, 
   isbn				= {9780780397040},
   pages				= {147--151}, 
   doi					= {10.1109/HEALTH.2006.246436},
   abstract			= {Not available}
}

@article{OC07,
   author          = {S. Oswald and R. Caldwell},
   title           = {Dispensing error rate after implementation of an automated pharmacy carousel system},
   journal         = {American Journal of Health-System Pharmacy},
   volume          = {64},
   number				= {13},
   month				= {July},
   year            = {2007},
   pages           = {1427--1431},
   issn            = {1079-2082},
   publisher       = {American Society of Health-System Pharmacists},
   address         = {Bethesda, MD USA},
   abstract        = {PURPOSE: A study was conducted to determine filling and dispensing error rates before 
and after the implementation of an automated pharmacy carousel system (APCS). METHODS: The study was 
conducted in a 613-bed acute and tertiary care university hospital. Before the implementation of the APCS, 
filling and dispensing rates were recorded during October through November 2004 and January 2005. 
Postimplementation data were collected during May through June 2006. Errors were recorded in three areas of 
pharmacy operations: first-dose or missing medication fill, automated dispensing cabinet fill, and 
interdepartmental request fill. A filling error was defined as an error caught by a pharmacist during the 
verification step. A dispensing error was defined as an error caught by a pharmacist observer after 
verification by the pharmacist. RESULTS: Before implementation of the APCS, 422 first-dose or missing 
medication orders were observed between October 2004 and January 2005. Independent data collected in 
December 2005, approximately six weeks after the introduction of the APCS, found that filling and error 
rates had increased. The filling rate for automated dispensing cabinets was associated with the largest 
decrease in errors. Filling and dispensing error rates had decreased by December 2005. In terms of 
interdepartmental request fill, no dispensing errors were noted in 123 clinic orders dispensed before the 
implementation of the APCS. One dispensing error out of 85 clinic orders was identified after 
implementation of the APCS. CONCLUSION: The implementation of an APCS at a university hospital decreased 
medication filling errors related to automated cabinets only and did not affect other filling and 
dispensing errors.}
}

@inproceedings{RojoEtAl08,
   author          = {M. G. Rojo and E. Rolon and L. Calahorra and F. O. Garcia and R. P. Sanchez 
   and F. Ruiz and N. Ballester and M. Armenteros and T. Rodriguez and R. M. Espartero},
   title           = {Implementation of the Business Process Modelling Notation (BPMN) in the modelling of 
anatomic pathology processes},
   booktitle			= {Proceedings of the 9th European Congress on Telepathology and 3rd International 
Congress on Virtual Microscopy},
   journal         = {Diagnostic Pathology},
   volume          = {3 (Suppl 1)},
   number		      = {S22}, 
   month				= {July},
   year            = {2008},
   doi					= {10.1186/1746-1596-3-S1-S22},
   issn            = {1746-1596},
   publisher       = {BioMed Central Ltd},
   address         = {London, UK},
   abstract        = {Background: Process orientation is one of the essential elements of quality management 
systems, including those in use in healthcare. Business processes in hospitals are very complex and 
variable. BPMN (Business Process Modelling Notation) is a user-oriented language specifically designed for 
the modelling of business (organizational) processes. Previous experiences of the use of this notation in 
the processes modelling within the Pathology in Spain or another country are not known. We present our 
experience in the elaboration of the conceptual models of Pathology processes, as part of a global 
programmed surgical patient process, using BPMN. Methods: With the objective of analyzing the use of BPMN 
notation in real cases, a multidisciplinary work group was created, including software engineers from the 
Dep. of Technologies and Information Systems from the University of Castilla-La Mancha and health 
professionals and administrative staff from the Hospital General de Ciudad Real. The work in collaboration 
was carried out in six phases: informative meetings, intensive training, process selection, definition of 
the work method, process describing by hospital experts, and process modelling. Results: The modelling of 
the processes of Anatomic Pathology is presented using BPMN. The presented subprocesses are those 
corresponding to the surgical pathology examination of the samples coming from operating theatre, including 
the planning and realization of frozen studies. Conclusion: The modelling of Anatomic Pathology 
subprocesses has allowed the creation of an understandable graphical model, where management and 
improvements are more easily implemented by health professionals}
}

@article{AMK09,
   author = {Amir Afrasiabi Rad and Morad Benyoucef and Craig E. Kuziemsky and Amir Afrasiabi Rad},
   title = {An evaluation framework for business process modeling languages in healthcare},
   journal = {J. Theor. Appl. Electron. Commer. Res.},
   volume = {4},
   issue = {2},
   month = {August},
   year = {2009},
   issn = {0718-1876},
   pages = {1--19},
   numpages = {19},
   doi = {10.1.1.189.2709},
   url = {http://dl.acm.org/citation.cfm?id=1807522.1807524},
   acmid = {1807524},
   publisher = {Facultad de Ingeniería, Universidad de Talca},
   address = {Talca, Chile},
}

@article{HKVM09,
   author          = {Barbara L. Hintzen and Scott J. Knoer and Christie J. Van Dyke and Brian S. 
   Milavitz},
   title           = {Effect of lean process improvement techniques on a university hospital inpatient 
pharmacy},
   journal         = {American Journal of Health-System Pharmacy},
   volume          = {66},
   number				= {22},
   month				= {November},
   year            = {2009},
   pages           = {2042--2047},
   issn            = {1079-2082},
   publisher       = {American Society of Health-System Pharmacists},
   address         = {Bethesda, MD USA},
   abstract        = {Purpose. The effect of lean process improvement on an inpatient university hospital 
pharmacy was evaluated. Summary. The University of Minnesota Medical Center (UMMC), Fairview, implemented 
lean techniques in its inpatient pharmacy to improve workflow, reduce waste, and achieve substantial cost 
savings. The sterile products area (SPA) and the inventory area were prospectively identified as locations 
for improvement due to their potential to realize cost savings. Process-improvement goals for the SPA 
included the reduction of missing doses, errors, and patient-specific waste by 30%, 50%, and 30%, 
%respectively, and the reallocation of two technician full-time equivalents (FTEs). Reductions in 
%pharmaceutical inventory and returns due to outdating were also anticipated. Work-flow in the SPA was 
%improved through the creation of accountability, standard work, and movement toward one-piece flow. 
%Increasing the number of i.v. batches decreased pharmaceutical waste by 40%. Through SPA environment 
%improvements and enhanced workload sharing, two FTE technicians from the SPA were redistributed within the 
%department. SPA waste reduction yielded an annual saving of $275,500. Quality and safety were also 
%improved, as measured by reductions in missing doses, expired products, and production errors. In the 
%inventory area, visual control was improved through the use of a double-bin system, the number of outdated 
%drugs decreased by 20%, and medication inventory was reduced by $50,000. Conclusion. Lean methodology was 
%successfully implemented in the SPA and inventory area at the UMMC, Fairview, inpatient pharmacy. Benefits 
%of this process included an estimated annual cost saving of $289,256 due to waste reduction, improvements 
%in workflow, and decreased staffing requirements.}
}

@incollection {PP09,
   author = {J. Puustjärvi and L. Puustjärvi},
   affiliation = {Helsinki University of Technology Box 9210 02015 TKK Finland},
   title = {Automating the Dissemination of Information Entities to Healthcare Professionals},
   booktitle = {Advances in Information Technology},
   series = {Communications in Computer and Information Science},
   editor = {Papasratorn, Borworn and Chutimaskul, Wichian and Porkaew, Kriengkrai and Vanijja, Vajirasak},
   publisher = {Springer Berlin Heidelberg},
   isbn = {978-3-642-10392-6},
   pages = {123-132},
   volume = {55},
   doi = {10.1007/978-3-642-10392-6_12},
   abstract = {Lifelong learning is a term that is widely used in a variety of context. The term 
   recognizes that learning is not confined to classroom, but takes place throughout life and in a 
   range of situations. A problem in lifelong learning is the dissemination of relevant learning 
   and informal material. Ideally, all the employees should receive all the relevant material 
   while not burden with irrelevant material. Neither the searching of the material should not 
   cause extra efforts. In trying to achieve these goals we have developed an Information entity 
   ontology, which captures learning material and the tasks of employees’ daily duties as well as 
   their relationships. This ontology allows (i) the integration of learning material with daily 
   duties, and (ii) the delivery of the material to relevant personnel. This kind of 
   dissemination, however, requires that the material is augmented by extra semantic information, 
   which is used in positioning the material into the Information entity ontology. Further in 
   order to avoid the efforts required for searching learning material, a workflow engine is 
   required for coordinating daily duties and attaching learning material to daily duties. In this 
   paper, we consider the deployment of such solutions in healthcare sector.},
   year = {2009}
}

@incollection {RGRPC10,
   author 			= {Elvira Rolón and Félix García and Francisco Ruíz and Mario Piattini and Luis 
   Calahorra},
   title 				= {Healthcare Process Development with BPMN},
   booktitle 		= {Handbook of Research on Developments in E-Health and Telemedicine: 
   Technological and Social Perspectives},
   editor 			= {Cruz-Cunha M. M., Tavares A. J., Simoes R.},
   year 				= {2010},
   pages 				= {1024--1047},
   doi 				= {10.4018/978-1-61520-670-4.ch049},
   isbn 				= {1615206701},
   publisher 		= {Facultad de Ingeniería, Universidad de Talca},
   address 			= {Talca, Chile},
   abstract = {The importance of the analysis, modelling and management of a business process is not 
   restricted to a specific enterprise sector. In the field of health management, as a result of the 
   nature of the service offered, health institutions’ processes are also the basis for decision 
   making which is focused on achieving their objective of providing quality medical assistance. In 
   this work, the authors shall present the application of business process modelling to the 
   processes of a health sector institution, using the BPMN standard notation. The objective of this 
   work is to show the experience obtained in the creation of the conceptual models of certain 
   hospital processes which can be used as a basis for others in collaboration with hospitals in 
   order to model their processes using BPMN. Hospital processes are highly complex, and their 
   graphical visualization facilitates their management and improvement by means of the 
   understanding and detection of possible failures.}
}

@article{Col10,
   author          = {Colquhoun, A.},
   title           = {Could automation improve efficieny and help pharmacies with cost saving?},
   journal         = {The Pharmaceutical Journal},
   volume          = {285},
   month				= {November},
   year            = {2010},
   issn            = {0031-687},
   pages           = {587--591},
   publisher       = {RPS Publishing},
   address         = {London, UK}
}

% BOOKS
%======
@book{BPMN2,
   author        = {Object Management Group},
   title         = {Business Process Model and Notation (BPMN) 2.0},
   publisher     = {Object Management Group},
   address       = {Needham MA, USA},
   url           = {http://www.omg.org/spec/BPMN/2.0/},
   year          = {2011}
}


% Unsorted
%=========
@unpublished{DDO07,
   title = {Formal Semantics and Analysis of BPMN Process Models},
   author = {Remco M. Dijkman and Marlon Dumas and Chun Ouyang},
   year = {2007},
   doi = {10.1.1.91.3621},
   url = {http://eprints.qut.edu.au/7115/},
   abstract = {The Business Process Modelling Notation (BPMN) is a standard for capturing business 
   processes in the early phases of system development. The mix of constructs in BPMN makes it 
   possible to define models with a range of semantic errors. But the static analysis of BPMN 
   models to detect such errors is hindered by ambiguities in the standard specification and the 
   complexity of the language. The fact that BPMN integrates constructs from graph-oriented 
   process definition languages with features for concurrent execution of multiple instances of a 
   subprocess and exception handling, makes it challenging to provide a formal semantics of BPMN. 
   Even more challenging is to provide a semantics that can be used to analyse BPMN models. This 
   paper proposes a formalisation of BPMN in terms a mapping to Petri nets, for which efficient 
   analysis techniques exist. The mapping has been implemented as a tool that generates code in 
   the Petri Net Markup Language. The formalisation has led to the identification of deficiencies 
   in the BPMN specification.}
}

@article{ODHA07,
   volume = {5},
   number = {1},
   author = {Chun Ouyang and Marlon Dumas and Arthur H. M. Ter Hofstede},
   title = {Pattern-based translation of BPMN process models to BPEL web services},
   publisher = {Idea Group Publishing},
   journal = {International Journal of Web Services Research (JWSR)},
   pages = {42--62},
   year = {2007},
   doi ={10.1.1.143.3118},
   url = {http://eprints.qut.edu.au/6810/},
   abstract = {The Business Process Modelling Notation (BPMN) is a graph-oriented language in
   which control and action nodes can be connected almost arbitrarily. It is primarily targeted at 
   domain analysts and is supported by many modelling tools, but in its current form, it lacks the 
   semantic precision required to capture fully executable business processes. The Business 
   Process Execution Language for Web Services (BPEL) on the other hand is a mainly 
   block-structured language, targeted at software developers and supported by several execution 
   platforms. In the current setting, translating BPMN models into BPEL code is a necessary step 
   towards standards-based business process development environments. This translation is 
   challenging since BPMN and BPEL represent two fundamentally different classes of languages. 
   Existing BPMN-to-BPEL translations rely on the identification of block-structured patterns in 
   BPMN models that are mapped into block-structured BPEL constructs. This paper advances the 
   state of the art in BPMN-to-BPEL translation by defining methods for identifying not only 
   perfectly block-structured fragments in BPMN models, but also quasi-structured fragments that 
   can be turned into perfectly structured ones and flow-based acyclic fragments that can be 
   mapped into a combination of block-structured constructs and control links. Beyond its direct 
   relevance in the context of BPMN and BPEL, this paper addresses issues that arise generally 
   when translating between graph-oriented and block-structured flow definition languages.}
}

@inproceedings{WG08,
   author = {Peter Y. Wong and Jeremy Gibbons},
   title = {A Process Semantics for BPMN},
   booktitle = {Proceedings of the 10th International Conference on Formal Methods and Software Engineering},
   series = {ICFEM '08},
   year = {2008},
   isbn = {978-3-540-88193-3},
   location = {Kitakyushu-City, Japan},
   pages = {355--374},
   numpages = {20},
   url = {http://dx.doi.org/10.1007/978-3-540-88194-0_22},
   doi = {http://dx.doi.org/10.1007/978-3-540-88194-0_22},
   acmid = {1483016},
   publisher = {Springer-Verlag},
   address = {Berlin, Heidelberg},
   abstract = {Business Process Modelling Notation (BPMN), developed by the Business Process 
   Management Initiative (BPMI), intends to bridge the gap between business process design and 
   implementation. However, the specification of the notation does not include a formal semantics. 
   This paper shows how a subset of the BPMN can be given a process semantics in Communicating 
   Sequential Processes. Such a semantics allows developers to formally analyse and compare BPMN 
   diagrams. A simple example of a business process is included to demonstrate the application of 
   the semantics; some theoretical results about the semantics are briefly discussed.}
} 

@article{KNP09,
   author = {Kwiatkowska, Marta and Norman, Gethin and Parker, David},
   title = {PRISM: probabilistic model checking for performance and reliability analysis},
   journal = {SIGMETRICS Perform. Eval. Rev.},
   volume = {36},
   issue = {4},
   month = {March},
   year = {2009},
   issn = {0163-5999},
   pages = {40--45},
   numpages = {6},
   url = {http://doi.acm.org/10.1145/1530873.1530882},
   doi = {http://doi.acm.org/10.1145/1530873.1530882},
   acmid = {1530882},
   publisher = {ACM},
   address = {New York, NY, USA},
   abstract = {Probabilistic model checking is a formal verification technique for the modelling 
   and analysis of stochastic systems. It has proved to be useful for studying a wide range of 
   quantitative properties of models taken from many diffierent application domains. This 
   includes, for example, performance and reliability properties of computer and communication 
   systems. In this paper, we give an overview of the probabilistic model checking tool PRISM, 
   focusing in particular on its support for continuous-time Markov chains and Markov reward 
   models, and how these can be used to analyse performability properties.}
} 

@inproceedings{KNP11,
   author={M. Kwiatkowska and G. Norman and D. Parker},
   title={{PRISM} 4.0: Verification of Probabilistic Real-time Systems},
   booktitle={Proc. 23rd International Conference on Computer Aided Verification (CAV'11)},
   year={2011},   
   editor={G. Gopalakrishnan and S. Qadeer},
   pages={585--591},
   organization={},
   publisher={Springer},
   series={LNCS},
   volume={6806},
   address={},
   month={},
   note={},
   key={}
}



@incollection{CGJLV00,
   author          = {Clarke, Edmund and Grumberg, Orna and Jha, Somesh and Lu, Yuan and Veith, Helmut},
   affiliation     = {Carnegie Mellon University, Pittsburgh USA USA},
   title           = {Counterexample-Guided Abstraction Refinement},
   booktitle       = {Computer Aided Verification},
   series          = {Lecture Notes in Computer Science},
   editor          = {Emerson, E. and Sistla, A.},
   publisher       = {Springer Berlin / Heidelberg},
   isbn            = {},
   pages           = {154-169},
   volume          = {1855},
   doi             = {10.1007/10722167_15},
   year            = {2000},
   abstract        = {We present an automatic iterative abstraction-refinement methodology in which the 
initial abstract model is generated by an automatic analysis of the control structures in the program to be 
verified. Abstract models may admit erroneous (or  spurious ) counterexamples. We devise new symbolic 
techniques which analyze such counterexamples and refine the abstract model correspondingly. The refinement 
algorithm keeps the size of the abstract state space small due to the use of abstraction functions which 
distinguish many degrees of abstraction for each program variable. We describe an implementation of our 
methodology in NuSMV. Practical experiments including a large Fujitsu IP core design with about 500 latches 
and 10000 lines of SMV code confirm the effectiveness of our approach.}   
}

@incollection{MPQV05,
   author          = {Mardare, Radu and Priami, Corrado and Quaglia, Paola and Vagin, Oleksandr},
   affiliation     = {Dipartimento di Informatica e Telecomunicazioni, Università di Trento Italy},
   title           = {Model Checking Biological Systems Described Using Ambient Calculus},
   booktitle       = {Computational Methods in Systems Biology},
   series          = {Lecture Notes in Computer Science},
   editor          = {Danos, Vincent and Schachter, Vincent},
   publisher       = {Springer Berlin / Heidelberg},
   isbn            = {},
   pages           = {85-103},
   volume          = {3082},
   doi             = {10.1007/978-3-540-25974-9_8},
   year            = {2005},
   abstract        = {We propose a way of performing model checking analysis for biological systems. The 
techniques were developed for a CTL* logic built upon Ambient Calculus.We introduce labelled syntax trees 
for ambient processes and use them as possible worlds in a Kripke structure developed for a propositional 
branching temporal logic. The accessibility relation over labelled syntax trees is generated by the 
reduction over corresponding Ambient Calculus processes.Providing the algorithms for calculating the 
accessibility relation between states, we open the perspective of using model checking algorithms developed 
for temporal logics in analysing any phenomena described in Ambient Calculus.}   
}

@inproceedings{FFK05,
   author          = {Fisteus, Jes\'{u}s Arias and Fern\'{a}ndez, Luis S\'{a}nchez and Kloos, Carlos Delgado},
   title           = {Applying model checking to BPEL4WS business collaborations},
   booktitle       = {SAC '05: Proceedings of the 2005 ACM symposium on Applied computing},
   year            = {2005},
   isbn            = {1-58113-964-0},
   pages           = {826--830},
   location        = {Santa Fe, New Mexico},
   doi             = {10.1145/1066677.1066866},
   publisher       = {ACM},
   address         = {New York, NY, USA},
   abstract        = {Web services are a very appropriate communication mechanism to perform distributed 
business processes among several organisations. These processes should be reliable, because a failure in 
them can cause high economic losses. In this work we propose a framework for the verification of business 
processes, called VERBUS. Its aim is to help the designer to find errors in specifications at design time, 
thus increasing their reliability. Contrary to verification frameworks previously proposed for business 
processes, VERBUS is a modular an extensible framework, in the sense that it is not tied to specific 
process definition languages or verification tools. This is achieved with the definition of an intermediate 
formalism that disconnects definition languages from verification tools. In this paper we present VERBUS, 
and its prototype, that integrates the BPEL4WS definition language and the Spin and SMV verification tools.}
}

@article{KNP09,
   author          = {Kwiatkowska, Marta and Norman, Gethin and Parker, David},
   title           = {PRISM: probabilistic model checking for performance and reliability analysis},
   journal         = {SIGMETRICS Perform. Eval. Rev.},
   volume          = {36},
   number          = {4},
   year            = {2009},
   issn            = {0163-5999},
   pages           = {40--45},
   doi             = {10.1145/1530873.1530882},
   publisher       = {ACM},
   address         = {New York, NY, USA},
   abstract        = {Probabilistic model checking is a formal verification technique for the modelling and 
analysis of stochastic systems. It has proved to be useful for studying a wide range of quantitative 
properties of models taken from many different application domains. This includes, for example, performance 
and reliability properties of computer and communication systems. In this paper, we give an overview of the 
probabilistic model checking tool PRISM, focusing in particular on its support for continuous-time Markov 
chains and Markov reward models, and how these can be used to analyse performability properties.}
}

% BOOKS (sorted chronologically)
%===============================
@book{McMillan93,
   author        = {McMillan, Kenneth L.},
   title         = {Symbolic Model Checking},
   isbn          = {0792393805},
   publisher     = {Kluwer Academic Publishers},
   address       = {Norwell, MA, USA},
   url           = {http://portal.acm.org/citation.cfm?id=530225},
   year          = {1993},
   abstract      = {Formal verification means having a mathematical model of a system, a language for 
specifying desired properties of the system in a concise, comprehensible and unambiguous way, and a method 
of proof to verify that the specified properties are satisfied. When the method of proof is carried out 
substantially by machine, we speak of automatic verification. Symbolic Model Checking deals with methods of 
automatic verification as applied to computer hardware.
   The practical motivation for study in this area is the high and increasing cost of correcting design errors 
in VLSI technologies. There is a growing demand for design methodologies that can yield correct designs on 
the first fabrication run. Moreover, design errors that are discovered before fabrication can also be quite 
costly, in terms of engineering effort required to correct the error, and the resulting impact on 
development schedules. Aside from pure cost considerations, there is also a need on the theoretical side to 
provide a sound mathematical basis for the design of computer systems, especially in areas that have 
received little theoretical attention.}
}

@book{BK08,
   author        = {Baier, Christel and Katoen, Joost-Pieter},
   howpublished  = {Hardcover},
   isbn          = {9780262026499},
   month         = {May},
   publisher     = {The MIT Press},
   title         = {Principles of Model Checking},
   url           = {http://mitpress.mit.edu/9780262026499},
   year          = {2008},
   abstract      = {Our growing dependence on increasingly complex computer and software systems necessitates 
the development of formalisms, techniques, and tools for assessing functional properties of these systems. 
One such technique that has emerged in the last twenty years is model checking, which systematically (and 
automatically) checks whether a model of a given system satisfies a desired property such as deadlock 
freedom, invariants, or request-response properties. This automated technique for verification and 
debugging has developed into a mature and widely used approach with many applications. Principles of Model 
Checking offers a comprehensive introduction to model checking that is not only a text suitable for 
classroom use but also a valuable reference for researchers and practitioners in the field.
   The book begins with the basic principles for modelling concurrent and communicating systems, introduces 
different classes of properties (including safety and liveness), presents the notion of fairness, and 
provides automata-based algorithms for these properties. It introduces the temporal logics LTL and CTL, 
compares them, and covers algorithms for verifying these logics, discussing real-time systems as well as 
systems subject to random phenomena. Separate chapters treat such efficiency-improving techniques as 
abstraction and symbolic manipulation. The book includes an extensive set of examples (most of which run 
through several chapters) and a complete set of basic results accompanied by detailed proofs. Each chapter 
concludes with a summary, bibliographic notes, and an extensive list of exercises of both practical and 
theoretical nature.}
}

@webpage{TuringAward07,
   title         = {ACM Turing Award Honors Founders of Automatic Verification Technology},
   url           = {http://www.acm.org/press-room/news-releases-2008/turing-award-07},
   author        = {The Association for Computing Machinery},
   lastchecked   = {27-09-2010}
}